Report for no_context/loop4.c

Generated on 2023-07-13 03:07:21 by CPAchecker 2.2 / svcomp23

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
extern void abort(void);  
2
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
3
void reach_error() { __assert_fail("0", "loop4.c", 10, "reach_error"); }  
4
void assume_abort_if_not(int cond) {  
5
  if(!cond) {abort();}  
6
}  
7
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }  
8
extern int __VERIFIER_nondet_int(void);  
9
extern void __VERIFIER_assume(int);  
10
  
11
int main() {  
12
    int x,y;  
13
    x = 0;  
14
    y = 0;  
15
    while (1) {  
16
        if (x < 50) {  
17
            y++;  
18
        } else {  
19
            y--;  
20
        }  
21
        if (y < 0) break;  
22
        x++;  
23
    }  
24
    __VERIFIER_assert(x == 100);  
25
    return 0;  
26
}  
DateTimeLevelComponentMessage
2023-07-1303:07:16:037INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2023-07-1303:07:16:054INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-07-1303:07:16:103INFOCPAchecker.runCPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-07-1303:07:16:119INFOCPAchecker.parseParsing CFA from file(s) "no_context/loop4.c"
2023-07-1303:07:16:922INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2023-07-1303:07:16:932WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.callstack.unsupportedFunctions
termination.violation.witness
cpa.predicate.memoryAllocationsAlwaysSucceed
cpa.arg.compressWitness
cpa.callstack.skipFunctionPointerRecursion
cpa.composite.aggregateBasicBlocks
counterexample.export.graphml
counterexample.export.compressWitness
cpa.arg.proofWitness
2023-07-1303:07:16:932INFOCPAchecker.runAlgorithmStarting analysis ...
2023-07-1303:07:16:936INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2023-07-1303:07:16:954INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 900s
2023-07-1303:07:16:957INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
CoreComponentsFactory.createAlgorithm
Using Restarting Algorithm
2023-07-1303:07:16:963INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
RestartAlgorithm.run
Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties ...
2023-07-1303:07:16:967INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-07-1303:07:16:968INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-07-1303:07:16:970INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-07-1303:07:16:972INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoop-symbolicExecution.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 140s
2023-07-1303:07:17:232INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
RestartAlgorithm.run
Starting analysis 1 ...
2023-07-1303:07:17:642INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set 0
Used algorithm property /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--singleLoopConfig.properties
Program containing only relevant bools 0
Relevant boolean vars / relevant vars ratio 0.1667
Requires alias handling 0
Requires loop handling 1
Has a single loop 1
Requires composite-type handling 0
Requires array handling 0
Requires float handling 0
Requires recursion handling 0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions true
Number of all righthand side functions 4
Restart Algorithm statistics
Number of algorithms provided 7
Number of algorithms used 1
Total time for algorithm 1 0.679s
ValueAnalysisCPA statistics
Number of variables per state 4.47 sum: 3204, count: 716, min: 0, max: 6
Number of global variables per state 0.00 sum: 0, count: 716, min: 0, max: 0
Number of assumptions 812
Number of deterministic assumptions 0
Level of Determinism 0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 715
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.014s
Total time for path thresholds 0.000s
SymbolicValueAnalysisPrecisionAdjustment statistics
Symbolic values before refinement 0 count: 715, min: 0, max: 0, avg: 0.00
Symbolic values after refinement 0 count: 715, min: 0, max: 0, avg: 0.00
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.003s
Replaced symbolic expressions 0
ConstraintsCPA statistics
Time for solving constraints 0.079s
Time for SMT check 0.000s
Time for resolving definites 0.000s
Cache lookups 203
Direct cache hits 202
Direct cache lookup time 0.000s
Subset cache hits 0
Subset cache lookup time 0.000s
Superset cache hits 0
Superset cache lookup time 0.000s
Number of removed outdated constraints 0 count: 203, min: 0, max: 0, avg: 0.00
Time for outdated constraint removal 0.009s
Constraints after refinement in state 0 count: 715, min: 0, max: 0, avg: 0.00
Constraints before refinement in state 0 count: 715, min: 0, max: 0, avg: 0.00
Time for constraints adjustment 0.005s
AutomatonAnalysis (SVCOMP) statistics
Number of states 1
Total time for successor computation 0.023s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 1129, count: 1129, min: 1, max: 1 [1 x 1129]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 716
Max size of waitlist 1
Average size of waitlist 1
Number of computed successors 715
Max successors for one state 1
Number of times merged 0
Number of times stopped 0
Number of times breaked 0
Total time for CPA algorithm 0.399s Max: 0.399s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.059s
Time for transfer relation 0.266s
Time for stop operator 0.054s
Time for adding to reached set 0.002s
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
CPA algorithm statistics
Number of iterations 716
Max size of waitlist 1
Average size of waitlist 1
Number of computed successors 715
Max successors for one state 1
Number of times merged 0
Number of times stopped 0
Number of times breaked 0
Total time for CPA algorithm 0.399s Max: 0.399s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.059s
Time for transfer relation 0.266s
Time for stop operator 0.054s
Time for adding to reached set 0.002s
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 0.500
Visited lines 12
Total lines 14
Line coverage 0.857
Visited conditions 5
Total conditions 8
Condition coverage 0.625
CPAchecker general statistics
Number of program locations 55
Number of CFA edges (per node) 52 count: 55, min: 0, max: 2, avg: 0.95
Number of relevant variables 6
Number of functions 4
Number of loops (and loop nodes) 1 sum: 15, min: 15, max: 15, avg: 15.00
Size of reached set 716
Number of reached locations 20 36%
Avg states per location 35
Max states per location 101 at node N25
Number of reached functions 2 50%
Number of target states 0
Time for analysis setup 0.813s
Time for loading CPAs 0.148s
Time for loading parser 0.161s
Time for CFA construction 0.475s
Time for parsing file(s) 0.228s
Time for AST to CFA 0.086s
Time for CFA sanity check 0.022s
Time for post-processing 0.072s
Time for CFA export 0.507s
Time for function pointers resolving 0.003s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.035s
Time for collecting variables 0.013s
Time for solving dependencies 0.001s
Time for building hierarchy 0.000s
Time for building classification 0.019s
Time for exporting data 0.002s
Time for Analysis 0.709s
CPU time for analysis 2.340s
Time for analyzing result 0.001s
Total time for CPAchecker 1.524s
Total CPU time for CPAchecker 4.650s
Time for statistics 0.138s
Time for Garbage Collector 0.041s in 4 runs
Garbage Collector(s) used G1 Old Generation, G1 Young Generation
Used heap memory 76MB ( 72 MiB) max; 38MB ( 36 MiB) avg; 95MB ( 91 MiB) peak
Used non-heap memory 40MB ( 38 MiB) max; 27MB ( 26 MiB) avg; 41MB ( 39 MiB) peak
Used in G1 Old Gen pool 13MB ( 12 MiB) max; 7MB ( 7 MiB) avg; 13MB ( 12 MiB) peak
Allocated heap memory 127MB ( 122 MiB) max; 127MB ( 122 MiB) avg
Allocated non-heap memory 44MB ( 42 MiB) max; 31MB ( 30 MiB) avg
Total process virtual memory 12286MB ( 11717 MiB) max; 12042MB ( 11484 MiB) avg
#Configuration NameConfiguration Value
1analysis.entryFunction main
2analysis.name svcomp23
3analysis.programNames no_context/loop4.c
4analysis.selectAnalysisHeuristically true
5analysis.summaryEdges true
6cfa.simplifyCfa false
7cfa.useCFACloningForMultiThreadedPrograms true
8counterexample.export.compressWitness false
9counterexample.export.graphml witness.graphml
10cpa.arg.compressWitness false
11cpa.arg.proofWitness witness.graphml
12cpa.callstack.skipFunctionPointerRecursion true
13cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14cpa.composite.aggregateBasicBlocks false
15cpa.predicate.memoryAllocationsAlwaysSucceed true
16datarace.config svcomp23--datarace.properties
17heuristicSelection.addressedRatio 0.0
18heuristicSelection.complexLoopConfig components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19heuristicSelection.loopConfig components/svcomp23--multipleLoopsConfig.properties
20heuristicSelection.loopFreeConfig components/svcomp23--configselection-restart-bmc-fallbacks.properties
21heuristicSelection.singleLoopConfig components/svcomp23--singleLoopConfig.properties
22language C
23limits.time.cpu 900s
24limits.time.cpu::required 900
25log.level INFO
26memorycleanup.config svcomp23--memorycleanup.properties
27memorysafety.config svcomp23--memorysafety.properties
28overflow.config svcomp23--overflow.properties
29parser.usePreprocessor true
30specification /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31statistics.print true
32termination.config svcomp23--termination.properties
33termination.violation.witness witness.graphml

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}